package merisis.traitspace;

import static java.lang.String.format;
import static merisis.util.BitUtil.bitsetOrArray;

import java.util.logging.Level;
import java.util.logging.Logger;

import merisis.MerisisVM;
import merisis.util.BitUtil;

import org.apache.solr.util.OpenBitSet;

import com.google.inject.Inject;

public class Morphism {

	@Inject
	private Logger logger;

	@Inject
	private MerisisVM mvm;

	public void set(long f, long a, long b) {

		long isainst = mvm.occur(a, f);
		long occurrence = mvm.occur(isainst, b);

		if (logger.isLoggable(Level.FINER)) {
			logger.finer(format("morphism %d:(%d:(%d %d), %d)", occurrence,
					isainst, a, f, b));
		}
	}

	public boolean exists(long f, long a, long b) {

		OpenBitSet checked = new OpenBitSet();
		OpenBitSet bs = new OpenBitSet();

		bs.set(a);

		boolean r = proof(checked, f, bs, b);

		if (logger.isLoggable(Level.FINEST)) {
			logger.finest(format("%s, %d:%d-->%d", (r ? "proofed" : "absurd"),
					f, a, b));
		}

		return r;
	}

	public long[] domain(long f, long b, boolean recursive) {

		OpenBitSet bs = new OpenBitSet();
		bs.set(b);

		return BitUtil.toArray(searchDomain(f, bs, new OpenBitSet(),
				new OpenBitSet(), recursive));
	}

	public long[] codomain(long f, long a, boolean isRecursive) {

		OpenBitSet checked = new OpenBitSet();
		OpenBitSet bs = new OpenBitSet();
		bs.set(a);

		return BitUtil.toArray(computeCodomain(f, bs, checked,
				new OpenBitSet(), isRecursive));
	}

	/**
	 * Proof the implications (f: a --> b).
	 * 
	 * @param f
	 *            the relation to be proofed
	 * @param a
	 * @param b
	 * @return
	 */
	public boolean proof(long f, long[][] a, long[][] b) {

		if (logger.isLoggable(Level.FINEST)) {
			logger.finest(String.format("proofing, %d: %s --> %s", f, BitUtil
					.toString(a), BitUtil.toString(b)));
		}

		OpenBitSet as = new OpenBitSet();
		for (int i = 0; i < a.length; i++) {

			long[] at = a[i];
			if (at.length == 1) {
				as.set(at[0]);
				continue;
			}

			OpenBitSet ats = null;
			for (int j = 0; j < at.length; j++) {

				long t = at[j];
				OpenBitSet ax;
				ax = bitsetOrArray(new OpenBitSet(), domain(f, t, true));
				ax.set(t);

				if (ats == null) {
					ats = new OpenBitSet();
					ats.or(ax);
					continue;
				}
				ats.and(ax);
			}

			if (ats != null)
				as.or(ats);
		}

		if (logger.isLoggable(Level.FINEST)) {
			logger.finest("antecedent: " + BitUtil.toString(as));
		}

		if (as.isEmpty())
			return true; // 0 --> t

		OpenBitSet bs = new OpenBitSet();
		for (int i = 0; i < b.length; i++) {

			long[] at = b[i];

			if (at.length == 1) {
				bs.set(at[0]);
				continue;
			}

			OpenBitSet ts = null;
			for (int j = 0; j < at.length; j++) {

				long t = at[j];
				OpenBitSet x;
				x = bitsetOrArray(new OpenBitSet(), domain(f, t, true));
				x.set(t);

				if (ts == null) {
					ts = new OpenBitSet();
					ts.or(x);
					continue;
				}
				ts.and(x);
			}

			bs.or(ts);
		}

		if (logger.isLoggable(Level.FINEST)) {
			logger.finest("sequent: " + BitUtil.toString(bs));
		}

		if (bs.isEmpty())
			return false; // t --> 0

		L: for (long ax = as.nextSetBit(0); ax >= 0; ax = as.nextSetBit(ax + 1)) {

			for (int i = 0; i < b.length; i++) {
				long[] bt = b[i];
				for (int j = 0; j < bt.length; j++) {
					if (exists(f, ax, bt[j]))
						continue L; // proofed ax --> b, next ax
				}
			}

			return false; // there is a absurd ax.
		}

		return true;
	}

	private OpenBitSet computeCodomain(long f, OpenBitSet todo,
			OpenBitSet checked, OpenBitSet result, boolean isRecursive) {

		for (long a = todo.nextSetBit(0); a >= 0; a = todo.nextSetBit(a + 1)) {

			if (checked.get(a))
				continue;

			todo.clear(a);
			checked.set(a);

			// OpenBitSet bparents = infimumB(new OpenBitSet(), f, a);
			OpenBitSet bparents = new OpenBitSet();
			searchCodomain(bparents, f, a);

			result.or(bparents);

			if (isRecursive)
				computeCodomain(f, bparents, checked, result, isRecursive);
		}

		return result;
	}

	private OpenBitSet searchDomain(long f, OpenBitSet todo,
			OpenBitSet checked, OpenBitSet result, boolean isRecursive) {

		for (long b = todo.nextSetBit(0); b >= 0; b = todo.nextSetBit(b + 1)) {

			if (checked.get(b))
				continue;

			todo.clear(b);
			checked.set(b);

			OpenBitSet aparents;
			aparents = new OpenBitSet();
			searchDomainOf(aparents, f, b);

			result.or(aparents);
			if (isRecursive)
				searchDomain(f, aparents, checked, result, isRecursive);
		}

		return result;
	}

	private boolean proof(OpenBitSet checked, long f, OpenBitSet from, long to) {

		for (long a = from.nextSetBit(0); a >= 0; a = from.nextSetBit(a + 1)) {

			// reflexivity
			if (a == to)
				return true;

			if (checked.get(a))
				continue;

			from.clear(a);
			checked.set(a);

			OpenBitSet bparents = new OpenBitSet();
			searchCodomain(bparents, f, a);

			if (bparents.get(to))
				return true;

			if (proof(checked, f, bparents, to))
				return true;
		}

		return false;
	}

	private void searchDomainOf(OpenBitSet result, long f, long to) {

		mvm.give(to, f);
		mvm.source();
		mvm.focus();
		mvm.autobeam();
		mvm.give(f);
		mvm.tprism();

		mvm.setfocus();

		mvm.autobeam();
		mvm.give(f);
		mvm.complement();

		long[] dots;
		dots = mvm.read();
		if (logger.isLoggable(Level.FINEST)) {
			logger.finest(String.format("%d's domain of %d: %s", f, to, BitUtil
					.toString(dots)));
		}

		if (dots == null)
			return;

		BitUtil.bitsetOrArray(result, dots);
	}

	private void searchCodomain(OpenBitSet result, long f, long from) {

		mvm.give(from, f);
		mvm.source();
		mvm.focus();
		mvm.autobeam();
		mvm.give(f);
		mvm.complement();

		long[] dots;
		dots = mvm.read();
		if (logger.isLoggable(Level.FINEST)) {
			logger.finest(String.format("%d's codomain of %d : %s", f, from,
					BitUtil.toString(dots)));
		}

		if (dots == null)
			return;

		BitUtil.bitsetOrArray(result, dots);
	}
}